perm filename DLO[1,JRA] blob sn#005855 filedate 1972-07-21 generic text, type T, neo UTF8
00100	LE(X1 X2) ∨ LE(X2 X1);
00200	(LE(X1 X2) ∧ LE(X2 X1))→ E(X1 X2);
00300	(LE(X1 X2) ∧ LE(X2 X3)) → LE(X1 X3);
00400	LE(X1 ADD1(X1));
00500	¬E(X1 ADD1(X1));
00600	LE(X2 X1) ∨ LE(ADD1(X1) X2);
00700	LE(X1 X1);
00800	;